basic
Irrefl(T;x,y.E(x;y)) == a:T. E(a;a) 

latex

Up	rel 1, rel 1
Wellformedness Lemmas	irrefl wf, irrefl wf
Definitions	x:A. B(x), A
FDL editor aliases	irrefl